↑ Goldstine and von Neumann. "Planning and Coding of problems for an Electronic Computing Instrument". Part II, Volume I, 1 April 1947, p. 12. "It may be true, that whenever C actually reaches a certain point in the flow diagram, one or more bound variables will necessarily possess certain specified values, or possess certain properties, or satisfy certain properties with each other. Furthermore, we may, at such a point, indicate the validity of these limitations. For this reason we will denote each area in which the validity of such limitations is being asserted, by a special box, which we call an assertion box."
↑ Alan Turing. Checking a Large Routine, 1949; quoted in C. A. R. Hoare, "The Emperor's Old Clothes", 1980 Turing Award lecture. "How can one check a large routine in the sense of making sure that it's right? In order that the man who checks may not have too difficult a task, the programmer should make a number of definite assertions which can be checked individually, and from which the correctness of the whole program easily follows"
